ds1, ds2:x:Id fp Type. ds2  ds1  State(ds1)  State(ds2) 

latex

Definitions	Id, t  T, Type, Top, f(x)?z, x:A. B(x), IdDeq, x.A(x), x. t(x), P  Q, State(ds), a:A fp B(a), f  g, False, A, x:AB(x), A & B, f(x), x:AB(x), Atom$n, if b t else f fi, b, s = t, b, , Prop, x:A. B(x), f(a), x  dom(f), P & Q, P  Q, Unit, left+right, type List, (x  l), {x:A| B(x) }, A/x,y. B(x;y), Void, Case b of inl(x)  s(x) ; inr(y)  t(y)
Lemmas	ifthenelse wf, l member wf, l member subtype, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, fpf-ap wf, bool wf, bnot wf, not wf, assert wf, fpf-sub wf, fpf wf, subtype rel dep function, fpf-cap wf, id-deq wf, top wf, subtype rel self, Id wf